// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_STRING_FILLER_MERGE_H
#define _sHT_STRING_FILLER_MERGE_H

#include <stddef.h>
#include <stdint.h>

#ifdef __FRAMA_C__
# include <sHT/string/setops.h>
#endif

/** Split a u16 string, filling the gap with zeroes */
/*@ requires dest_w: \valid(&dest[0 .. n - 1]);
    requires dest_w0S: \valid(&dest[0]);
    requires from_r: \valid_read(&from[0 .. end - 1]);
    requires from_r0S: \valid_read(&from[0]);
    requires from_s: \initialized(&from[0 .. end - 1]);
    requires from_s0S: \initialized(&from[0]);
    requires d: \separated(&dest[0 .. n - 1], &from[0 .. n - 1]);
    requires r: brk <= end <= n;
    terminates \true;
    assigns dest[0], dest[0 .. n - 1] \from from[0 .. n - 1], from[0];
    ensures dest0_NS: memeq16{Post,Pre}(dest, from, brk);
    ensures dest1_NS: bzero16{Post}(dest + brk, n - end);
    ensures dest2_NS: memeq16{Post,Pre}(dest + (brk + n - end), from + brk, end - brk);
    ensures dest_sNS: \initialized(&dest[0 .. n - 1]); */
void
sHT_merge16(uint16_t dest[], const uint16_t from[], size_t n, size_t brk, size_t end);

#endif
